package systemf;

import java.util.Objects;

/**
 * System F类型系统
 * 支持基本类型、函数类型和全称类型（∀）
 */
public abstract class Type {
    
    /**
     * 基本类型
     */
    public static class BaseType extends Type {
        private final String name;
        
        public BaseType(String name) {
            this.name = name;
        }
        
        public String getName() {
            return name;
        }
        
        @Override
        public String toString() {
            return name;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            BaseType baseType = (BaseType) o;
            return Objects.equals(name, baseType.name);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(name);
        }
    }
    
    /**
     * 函数类型 τ → σ
     */
    public static class ArrowType extends Type {
        private final Type domain;
        private final Type codomain;
        
        public ArrowType(Type domain, Type codomain) {
            this.domain = domain;
            this.codomain = codomain;
        }
        
        public Type getDomain() {
            return domain;
        }
        
        public Type getCodomain() {
            return codomain;
        }
        
        @Override
        public String toString() {
            String domainStr = domain instanceof ArrowType 
                ? "(" + domain + ")" 
                : domain.toString();
            return domainStr + " → " + codomain;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            ArrowType arrowType = (ArrowType) o;
            return Objects.equals(domain, arrowType.domain) &&
                   Objects.equals(codomain, arrowType.codomain);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(domain, codomain);
        }
    }
    
    /**
     * 全称类型 ∀α.τ
     */
    public static class ForallType extends Type {
        private final String typeVar;
        private final Type body;
        
        public ForallType(String typeVar, Type body) {
            this.typeVar = typeVar;
            this.body = body;
        }
        
        public String getTypeVar() {
            return typeVar;
        }
        
        public Type getBody() {
            return body;
        }
        
        @Override
        public String toString() {
            return "∀" + typeVar + "." + body;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            ForallType that = (ForallType) o;
            // α-等价：需要重命名比较
            return Objects.equals(typeVar, that.typeVar) &&
                   Objects.equals(body, that.body);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(typeVar, body);
        }
    }
    
    /**
     * 类型变量（用于类型检查）
     */
    public static class TypeVar extends Type {
        private final String name;
        
        public TypeVar(String name) {
            this.name = name;
        }
        
        public String getName() {
            return name;
        }
        
        @Override
        public String toString() {
            return name;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            TypeVar typeVar = (TypeVar) o;
            return Objects.equals(name, typeVar.name);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(name);
        }
    }
    
    /**
     * 类型替换：将类型变量α替换为类型τ
     */
    public Type substitute(String typeVar, Type replacement) {
        if (this instanceof TypeVar && ((TypeVar) this).getName().equals(typeVar)) {
            return replacement;
        } else if (this instanceof ArrowType) {
            ArrowType arrow = (ArrowType) this;
            return new ArrowType(
                arrow.domain.substitute(typeVar, replacement),
                arrow.codomain.substitute(typeVar, replacement)
            );
        } else if (this instanceof ForallType) {
            ForallType forall = (ForallType) this;
            if (forall.typeVar.equals(typeVar)) {
                return this; // 绑定变量，不替换
            }
            return new ForallType(
                forall.typeVar,
                forall.body.substitute(typeVar, replacement)
            );
        }
        return this;
    }
}

